the_es:ES, e:E, l:IdLnk, m:Msg.
(m  sends(l;e))
 e':rvc(l,mtag(m),v).(e < e')
 & ((msgtype(m) = valtype(e')  Type) c (v = mval(m)  valtype(e'))) 

latex

Definitions	x:A. B(x), P  Q, (x  l), e:rvc(l,tg,v).P(e;v), P & Q, A c B, A, {i..j}, x:A. B(x), t  T, A  B, i  j < k, , S  T, False, T, True, mtag(m), msg(l;t;v), mtag(m), t.1, t.2, mval(m), (Msg on l), , mval(m)
Lemmas	es-axioms, le wf, length wf1, es-Msgl wf, es-sends wf, assert wf, es-isrcv wf, es-lnk wf, Id wf, es-tag wf, es-mtag wf, es-causl wf, es-msgtype wf, es-valtype wf, es-val wf, es-mval wf, nat wf, es-Msg wf, select wf, IdLnk wf, es-E wf, event system wf, squash wf, true wf, es-mval-valtype, es-sender-causl